Search Results

Documents authored by Vaux Auclair, Lionel

Document
DOI: 10.4230/LIPIcs.FSCD.2023.13
Strategies as Resource Terms, and Their Categorical Semantics

Authors: Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
As shown by Tsukada and Ong, simply-typed, normal and η-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. Though inspiring, their proof is indirect, relying on the injectivity of the relational model {w.r.t.} both sides of the correspondence - in particular, the dynamics of the resource calculus is taken into account only via the compatibility of the relational model with the composition of normal terms defined by normalization. In the present paper, we revisit and extend these results. Our first contribution is to restate the correspondence by considering causal structures we call augmentations, which are canonical representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit account of the connection with normal resource terms. As a second contribution, we extend this account to the reduction of resource terms: building on a notion of strategies as weighted sums of augmentations, we provide a denotational model of the resource calculus, invariant under reduction. A key step - and our third contribution - is a categorical model we call a resource category, which is to the resource calculus what differential categories are to the differential λ-calculus.
Cite as

Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair. Strategies as Resource Terms, and Their Categorical Semantics. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{blondeaupatissier_et_al:LIPIcs.FSCD.2023.13,
  author =	{Blondeau-Patissier, Lison and Clairambault, Pierre and Vaux Auclair, Lionel},
  title =	{{Strategies as Resource Terms, and Their Categorical Semantics}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.13},
  URN =		{urn:nbn:de:0030-drops-179976},
  doi =		{10.4230/LIPIcs.FSCD.2023.13},
  annote =	{Keywords: Resource calculus, Game semantics, Categorical semantics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.15
An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets

Authors: Jules Chouquet and Lionel Vaux Auclair

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose some constraint on switching paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction. Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative exponential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfy our constraints. In the present work, we stick to the unit-free and weakening-free fragment of linear logic, which is rich enough to showcase our techniques, while allowing for a very simple kind of constraint: a bound on the number of cuts that are crossed by any switching path.
Cite as

Jules Chouquet and Lionel Vaux Auclair. An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{chouquet_et_al:LIPIcs.CSL.2018.15,
  author =	{Chouquet, Jules and Vaux Auclair, Lionel},
  title =	{{An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.15},
  URN =		{urn:nbn:de:0030-drops-96828},
  doi =		{10.4230/LIPIcs.CSL.2018.15},
  annote =	{Keywords: linear logic, proof nets, cut elimination, differential linear logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact